Left Termination of the query pattern prime_in_1(g) w.r.t. the given Prolog program could successfully be proven:



↳ Prolog
  ↳ PrologToPiTRSProof

Clauses:

div(X, Y, Z) :- quot(X, Y, Y, Z).
quot(0, s(Y), s(Z), 0).
quot(s(X), s(Y), Z, U) :- quot(X, Y, Z, U).
quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U).
prime(s(s(X))) :- pr(s(s(X)), s(X)).
pr(X, s(0)).
pr(X, s(s(Y))) :- ','(not_divides(s(s(Y)), X), pr(X, s(Y))).
not_divides(Y, X) :- ','(div(X, Y, U), ','(times(U, Y, Z), neq(X, Z))).
neq(s(X), 0).
neq(0, s(X)).
neq(s(X), s(Y)) :- neq(X, Y).
times(0, Y, 0).
times(s(X), Y, Z) :- ','(times(X, Y, U), add(U, Y, Z)).
add(X, 0, X).
add(0, X, X).
add(s(X), Y, s(Z)) :- add(X, Y, Z).

Queries:

prime(g).

We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
prime_in: (b)
pr_in: (b,b)
not_divides_in: (b,b)
div_in: (b,b,f)
quot_in: (b,b,b,f)
times_in: (b,b,f)
add_in: (b,b,f)
neq_in: (b,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

prime_in_g(s(s(X))) → U4_g(X, pr_in_gg(s(s(X)), s(X)))
pr_in_gg(X, s(0)) → pr_out_gg(X, s(0))
pr_in_gg(X, s(s(Y))) → U5_gg(X, Y, not_divides_in_gg(s(s(Y)), X))
not_divides_in_gg(Y, X) → U7_gg(Y, X, div_in_gga(X, Y, U))
div_in_gga(X, Y, Z) → U1_gga(X, Y, Z, quot_in_ggga(X, Y, Y, Z))
quot_in_ggga(0, s(Y), s(Z), 0) → quot_out_ggga(0, s(Y), s(Z), 0)
quot_in_ggga(s(X), s(Y), Z, U) → U2_ggga(X, Y, Z, U, quot_in_ggga(X, Y, Z, U))
quot_in_ggga(X, 0, s(Z), s(U)) → U3_ggga(X, Z, U, quot_in_ggga(X, s(Z), s(Z), U))
U3_ggga(X, Z, U, quot_out_ggga(X, s(Z), s(Z), U)) → quot_out_ggga(X, 0, s(Z), s(U))
U2_ggga(X, Y, Z, U, quot_out_ggga(X, Y, Z, U)) → quot_out_ggga(s(X), s(Y), Z, U)
U1_gga(X, Y, Z, quot_out_ggga(X, Y, Y, Z)) → div_out_gga(X, Y, Z)
U7_gg(Y, X, div_out_gga(X, Y, U)) → U8_gg(Y, X, times_in_gga(U, Y, Z))
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U11_gga(X, Y, Z, times_in_gga(X, Y, U))
U11_gga(X, Y, Z, times_out_gga(X, Y, U)) → U12_gga(X, Y, Z, add_in_gga(U, Y, Z))
add_in_gga(X, 0, X) → add_out_gga(X, 0, X)
add_in_gga(0, X, X) → add_out_gga(0, X, X)
add_in_gga(s(X), Y, s(Z)) → U13_gga(X, Y, Z, add_in_gga(X, Y, Z))
U13_gga(X, Y, Z, add_out_gga(X, Y, Z)) → add_out_gga(s(X), Y, s(Z))
U12_gga(X, Y, Z, add_out_gga(U, Y, Z)) → times_out_gga(s(X), Y, Z)
U8_gg(Y, X, times_out_gga(U, Y, Z)) → U9_gg(Y, X, neq_in_gg(X, Z))
neq_in_gg(s(X), 0) → neq_out_gg(s(X), 0)
neq_in_gg(0, s(X)) → neq_out_gg(0, s(X))
neq_in_gg(s(X), s(Y)) → U10_gg(X, Y, neq_in_gg(X, Y))
U10_gg(X, Y, neq_out_gg(X, Y)) → neq_out_gg(s(X), s(Y))
U9_gg(Y, X, neq_out_gg(X, Z)) → not_divides_out_gg(Y, X)
U5_gg(X, Y, not_divides_out_gg(s(s(Y)), X)) → U6_gg(X, Y, pr_in_gg(X, s(Y)))
U6_gg(X, Y, pr_out_gg(X, s(Y))) → pr_out_gg(X, s(s(Y)))
U4_g(X, pr_out_gg(s(s(X)), s(X))) → prime_out_g(s(s(X)))

The argument filtering Pi contains the following mapping:
prime_in_g(x1)  =  prime_in_g(x1)
s(x1)  =  s(x1)
U4_g(x1, x2)  =  U4_g(x2)
pr_in_gg(x1, x2)  =  pr_in_gg(x1, x2)
0  =  0
pr_out_gg(x1, x2)  =  pr_out_gg
U5_gg(x1, x2, x3)  =  U5_gg(x1, x2, x3)
not_divides_in_gg(x1, x2)  =  not_divides_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
div_in_gga(x1, x2, x3)  =  div_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x4)
quot_in_ggga(x1, x2, x3, x4)  =  quot_in_ggga(x1, x2, x3)
quot_out_ggga(x1, x2, x3, x4)  =  quot_out_ggga(x4)
U2_ggga(x1, x2, x3, x4, x5)  =  U2_ggga(x5)
U3_ggga(x1, x2, x3, x4)  =  U3_ggga(x4)
div_out_gga(x1, x2, x3)  =  div_out_gga(x3)
U8_gg(x1, x2, x3)  =  U8_gg(x2, x3)
times_in_gga(x1, x2, x3)  =  times_in_gga(x1, x2)
times_out_gga(x1, x2, x3)  =  times_out_gga(x3)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x2, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
add_in_gga(x1, x2, x3)  =  add_in_gga(x1, x2)
add_out_gga(x1, x2, x3)  =  add_out_gga(x3)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x4)
U9_gg(x1, x2, x3)  =  U9_gg(x3)
neq_in_gg(x1, x2)  =  neq_in_gg(x1, x2)
neq_out_gg(x1, x2)  =  neq_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
not_divides_out_gg(x1, x2)  =  not_divides_out_gg
U6_gg(x1, x2, x3)  =  U6_gg(x3)
prime_out_g(x1)  =  prime_out_g

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

prime_in_g(s(s(X))) → U4_g(X, pr_in_gg(s(s(X)), s(X)))
pr_in_gg(X, s(0)) → pr_out_gg(X, s(0))
pr_in_gg(X, s(s(Y))) → U5_gg(X, Y, not_divides_in_gg(s(s(Y)), X))
not_divides_in_gg(Y, X) → U7_gg(Y, X, div_in_gga(X, Y, U))
div_in_gga(X, Y, Z) → U1_gga(X, Y, Z, quot_in_ggga(X, Y, Y, Z))
quot_in_ggga(0, s(Y), s(Z), 0) → quot_out_ggga(0, s(Y), s(Z), 0)
quot_in_ggga(s(X), s(Y), Z, U) → U2_ggga(X, Y, Z, U, quot_in_ggga(X, Y, Z, U))
quot_in_ggga(X, 0, s(Z), s(U)) → U3_ggga(X, Z, U, quot_in_ggga(X, s(Z), s(Z), U))
U3_ggga(X, Z, U, quot_out_ggga(X, s(Z), s(Z), U)) → quot_out_ggga(X, 0, s(Z), s(U))
U2_ggga(X, Y, Z, U, quot_out_ggga(X, Y, Z, U)) → quot_out_ggga(s(X), s(Y), Z, U)
U1_gga(X, Y, Z, quot_out_ggga(X, Y, Y, Z)) → div_out_gga(X, Y, Z)
U7_gg(Y, X, div_out_gga(X, Y, U)) → U8_gg(Y, X, times_in_gga(U, Y, Z))
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U11_gga(X, Y, Z, times_in_gga(X, Y, U))
U11_gga(X, Y, Z, times_out_gga(X, Y, U)) → U12_gga(X, Y, Z, add_in_gga(U, Y, Z))
add_in_gga(X, 0, X) → add_out_gga(X, 0, X)
add_in_gga(0, X, X) → add_out_gga(0, X, X)
add_in_gga(s(X), Y, s(Z)) → U13_gga(X, Y, Z, add_in_gga(X, Y, Z))
U13_gga(X, Y, Z, add_out_gga(X, Y, Z)) → add_out_gga(s(X), Y, s(Z))
U12_gga(X, Y, Z, add_out_gga(U, Y, Z)) → times_out_gga(s(X), Y, Z)
U8_gg(Y, X, times_out_gga(U, Y, Z)) → U9_gg(Y, X, neq_in_gg(X, Z))
neq_in_gg(s(X), 0) → neq_out_gg(s(X), 0)
neq_in_gg(0, s(X)) → neq_out_gg(0, s(X))
neq_in_gg(s(X), s(Y)) → U10_gg(X, Y, neq_in_gg(X, Y))
U10_gg(X, Y, neq_out_gg(X, Y)) → neq_out_gg(s(X), s(Y))
U9_gg(Y, X, neq_out_gg(X, Z)) → not_divides_out_gg(Y, X)
U5_gg(X, Y, not_divides_out_gg(s(s(Y)), X)) → U6_gg(X, Y, pr_in_gg(X, s(Y)))
U6_gg(X, Y, pr_out_gg(X, s(Y))) → pr_out_gg(X, s(s(Y)))
U4_g(X, pr_out_gg(s(s(X)), s(X))) → prime_out_g(s(s(X)))

The argument filtering Pi contains the following mapping:
prime_in_g(x1)  =  prime_in_g(x1)
s(x1)  =  s(x1)
U4_g(x1, x2)  =  U4_g(x2)
pr_in_gg(x1, x2)  =  pr_in_gg(x1, x2)
0  =  0
pr_out_gg(x1, x2)  =  pr_out_gg
U5_gg(x1, x2, x3)  =  U5_gg(x1, x2, x3)
not_divides_in_gg(x1, x2)  =  not_divides_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
div_in_gga(x1, x2, x3)  =  div_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x4)
quot_in_ggga(x1, x2, x3, x4)  =  quot_in_ggga(x1, x2, x3)
quot_out_ggga(x1, x2, x3, x4)  =  quot_out_ggga(x4)
U2_ggga(x1, x2, x3, x4, x5)  =  U2_ggga(x5)
U3_ggga(x1, x2, x3, x4)  =  U3_ggga(x4)
div_out_gga(x1, x2, x3)  =  div_out_gga(x3)
U8_gg(x1, x2, x3)  =  U8_gg(x2, x3)
times_in_gga(x1, x2, x3)  =  times_in_gga(x1, x2)
times_out_gga(x1, x2, x3)  =  times_out_gga(x3)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x2, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
add_in_gga(x1, x2, x3)  =  add_in_gga(x1, x2)
add_out_gga(x1, x2, x3)  =  add_out_gga(x3)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x4)
U9_gg(x1, x2, x3)  =  U9_gg(x3)
neq_in_gg(x1, x2)  =  neq_in_gg(x1, x2)
neq_out_gg(x1, x2)  =  neq_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
not_divides_out_gg(x1, x2)  =  not_divides_out_gg
U6_gg(x1, x2, x3)  =  U6_gg(x3)
prime_out_g(x1)  =  prime_out_g


Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

PRIME_IN_G(s(s(X))) → U4_G(X, pr_in_gg(s(s(X)), s(X)))
PRIME_IN_G(s(s(X))) → PR_IN_GG(s(s(X)), s(X))
PR_IN_GG(X, s(s(Y))) → U5_GG(X, Y, not_divides_in_gg(s(s(Y)), X))
PR_IN_GG(X, s(s(Y))) → NOT_DIVIDES_IN_GG(s(s(Y)), X)
NOT_DIVIDES_IN_GG(Y, X) → U7_GG(Y, X, div_in_gga(X, Y, U))
NOT_DIVIDES_IN_GG(Y, X) → DIV_IN_GGA(X, Y, U)
DIV_IN_GGA(X, Y, Z) → U1_GGA(X, Y, Z, quot_in_ggga(X, Y, Y, Z))
DIV_IN_GGA(X, Y, Z) → QUOT_IN_GGGA(X, Y, Y, Z)
QUOT_IN_GGGA(s(X), s(Y), Z, U) → U2_GGGA(X, Y, Z, U, quot_in_ggga(X, Y, Z, U))
QUOT_IN_GGGA(s(X), s(Y), Z, U) → QUOT_IN_GGGA(X, Y, Z, U)
QUOT_IN_GGGA(X, 0, s(Z), s(U)) → U3_GGGA(X, Z, U, quot_in_ggga(X, s(Z), s(Z), U))
QUOT_IN_GGGA(X, 0, s(Z), s(U)) → QUOT_IN_GGGA(X, s(Z), s(Z), U)
U7_GG(Y, X, div_out_gga(X, Y, U)) → U8_GG(Y, X, times_in_gga(U, Y, Z))
U7_GG(Y, X, div_out_gga(X, Y, U)) → TIMES_IN_GGA(U, Y, Z)
TIMES_IN_GGA(s(X), Y, Z) → U11_GGA(X, Y, Z, times_in_gga(X, Y, U))
TIMES_IN_GGA(s(X), Y, Z) → TIMES_IN_GGA(X, Y, U)
U11_GGA(X, Y, Z, times_out_gga(X, Y, U)) → U12_GGA(X, Y, Z, add_in_gga(U, Y, Z))
U11_GGA(X, Y, Z, times_out_gga(X, Y, U)) → ADD_IN_GGA(U, Y, Z)
ADD_IN_GGA(s(X), Y, s(Z)) → U13_GGA(X, Y, Z, add_in_gga(X, Y, Z))
ADD_IN_GGA(s(X), Y, s(Z)) → ADD_IN_GGA(X, Y, Z)
U8_GG(Y, X, times_out_gga(U, Y, Z)) → U9_GG(Y, X, neq_in_gg(X, Z))
U8_GG(Y, X, times_out_gga(U, Y, Z)) → NEQ_IN_GG(X, Z)
NEQ_IN_GG(s(X), s(Y)) → U10_GG(X, Y, neq_in_gg(X, Y))
NEQ_IN_GG(s(X), s(Y)) → NEQ_IN_GG(X, Y)
U5_GG(X, Y, not_divides_out_gg(s(s(Y)), X)) → U6_GG(X, Y, pr_in_gg(X, s(Y)))
U5_GG(X, Y, not_divides_out_gg(s(s(Y)), X)) → PR_IN_GG(X, s(Y))

The TRS R consists of the following rules:

prime_in_g(s(s(X))) → U4_g(X, pr_in_gg(s(s(X)), s(X)))
pr_in_gg(X, s(0)) → pr_out_gg(X, s(0))
pr_in_gg(X, s(s(Y))) → U5_gg(X, Y, not_divides_in_gg(s(s(Y)), X))
not_divides_in_gg(Y, X) → U7_gg(Y, X, div_in_gga(X, Y, U))
div_in_gga(X, Y, Z) → U1_gga(X, Y, Z, quot_in_ggga(X, Y, Y, Z))
quot_in_ggga(0, s(Y), s(Z), 0) → quot_out_ggga(0, s(Y), s(Z), 0)
quot_in_ggga(s(X), s(Y), Z, U) → U2_ggga(X, Y, Z, U, quot_in_ggga(X, Y, Z, U))
quot_in_ggga(X, 0, s(Z), s(U)) → U3_ggga(X, Z, U, quot_in_ggga(X, s(Z), s(Z), U))
U3_ggga(X, Z, U, quot_out_ggga(X, s(Z), s(Z), U)) → quot_out_ggga(X, 0, s(Z), s(U))
U2_ggga(X, Y, Z, U, quot_out_ggga(X, Y, Z, U)) → quot_out_ggga(s(X), s(Y), Z, U)
U1_gga(X, Y, Z, quot_out_ggga(X, Y, Y, Z)) → div_out_gga(X, Y, Z)
U7_gg(Y, X, div_out_gga(X, Y, U)) → U8_gg(Y, X, times_in_gga(U, Y, Z))
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U11_gga(X, Y, Z, times_in_gga(X, Y, U))
U11_gga(X, Y, Z, times_out_gga(X, Y, U)) → U12_gga(X, Y, Z, add_in_gga(U, Y, Z))
add_in_gga(X, 0, X) → add_out_gga(X, 0, X)
add_in_gga(0, X, X) → add_out_gga(0, X, X)
add_in_gga(s(X), Y, s(Z)) → U13_gga(X, Y, Z, add_in_gga(X, Y, Z))
U13_gga(X, Y, Z, add_out_gga(X, Y, Z)) → add_out_gga(s(X), Y, s(Z))
U12_gga(X, Y, Z, add_out_gga(U, Y, Z)) → times_out_gga(s(X), Y, Z)
U8_gg(Y, X, times_out_gga(U, Y, Z)) → U9_gg(Y, X, neq_in_gg(X, Z))
neq_in_gg(s(X), 0) → neq_out_gg(s(X), 0)
neq_in_gg(0, s(X)) → neq_out_gg(0, s(X))
neq_in_gg(s(X), s(Y)) → U10_gg(X, Y, neq_in_gg(X, Y))
U10_gg(X, Y, neq_out_gg(X, Y)) → neq_out_gg(s(X), s(Y))
U9_gg(Y, X, neq_out_gg(X, Z)) → not_divides_out_gg(Y, X)
U5_gg(X, Y, not_divides_out_gg(s(s(Y)), X)) → U6_gg(X, Y, pr_in_gg(X, s(Y)))
U6_gg(X, Y, pr_out_gg(X, s(Y))) → pr_out_gg(X, s(s(Y)))
U4_g(X, pr_out_gg(s(s(X)), s(X))) → prime_out_g(s(s(X)))

The argument filtering Pi contains the following mapping:
prime_in_g(x1)  =  prime_in_g(x1)
s(x1)  =  s(x1)
U4_g(x1, x2)  =  U4_g(x2)
pr_in_gg(x1, x2)  =  pr_in_gg(x1, x2)
0  =  0
pr_out_gg(x1, x2)  =  pr_out_gg
U5_gg(x1, x2, x3)  =  U5_gg(x1, x2, x3)
not_divides_in_gg(x1, x2)  =  not_divides_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
div_in_gga(x1, x2, x3)  =  div_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x4)
quot_in_ggga(x1, x2, x3, x4)  =  quot_in_ggga(x1, x2, x3)
quot_out_ggga(x1, x2, x3, x4)  =  quot_out_ggga(x4)
U2_ggga(x1, x2, x3, x4, x5)  =  U2_ggga(x5)
U3_ggga(x1, x2, x3, x4)  =  U3_ggga(x4)
div_out_gga(x1, x2, x3)  =  div_out_gga(x3)
U8_gg(x1, x2, x3)  =  U8_gg(x2, x3)
times_in_gga(x1, x2, x3)  =  times_in_gga(x1, x2)
times_out_gga(x1, x2, x3)  =  times_out_gga(x3)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x2, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
add_in_gga(x1, x2, x3)  =  add_in_gga(x1, x2)
add_out_gga(x1, x2, x3)  =  add_out_gga(x3)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x4)
U9_gg(x1, x2, x3)  =  U9_gg(x3)
neq_in_gg(x1, x2)  =  neq_in_gg(x1, x2)
neq_out_gg(x1, x2)  =  neq_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
not_divides_out_gg(x1, x2)  =  not_divides_out_gg
U6_gg(x1, x2, x3)  =  U6_gg(x3)
prime_out_g(x1)  =  prime_out_g
U5_GG(x1, x2, x3)  =  U5_GG(x1, x2, x3)
DIV_IN_GGA(x1, x2, x3)  =  DIV_IN_GGA(x1, x2)
TIMES_IN_GGA(x1, x2, x3)  =  TIMES_IN_GGA(x1, x2)
QUOT_IN_GGGA(x1, x2, x3, x4)  =  QUOT_IN_GGGA(x1, x2, x3)
U11_GGA(x1, x2, x3, x4)  =  U11_GGA(x2, x4)
NEQ_IN_GG(x1, x2)  =  NEQ_IN_GG(x1, x2)
U2_GGGA(x1, x2, x3, x4, x5)  =  U2_GGGA(x5)
U12_GGA(x1, x2, x3, x4)  =  U12_GGA(x4)
ADD_IN_GGA(x1, x2, x3)  =  ADD_IN_GGA(x1, x2)
U6_GG(x1, x2, x3)  =  U6_GG(x3)
NOT_DIVIDES_IN_GG(x1, x2)  =  NOT_DIVIDES_IN_GG(x1, x2)
U4_G(x1, x2)  =  U4_G(x2)
U9_GG(x1, x2, x3)  =  U9_GG(x3)
PRIME_IN_G(x1)  =  PRIME_IN_G(x1)
U10_GG(x1, x2, x3)  =  U10_GG(x3)
U13_GGA(x1, x2, x3, x4)  =  U13_GGA(x4)
U3_GGGA(x1, x2, x3, x4)  =  U3_GGGA(x4)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x4)
U7_GG(x1, x2, x3)  =  U7_GG(x1, x2, x3)
U8_GG(x1, x2, x3)  =  U8_GG(x2, x3)
PR_IN_GG(x1, x2)  =  PR_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

PRIME_IN_G(s(s(X))) → U4_G(X, pr_in_gg(s(s(X)), s(X)))
PRIME_IN_G(s(s(X))) → PR_IN_GG(s(s(X)), s(X))
PR_IN_GG(X, s(s(Y))) → U5_GG(X, Y, not_divides_in_gg(s(s(Y)), X))
PR_IN_GG(X, s(s(Y))) → NOT_DIVIDES_IN_GG(s(s(Y)), X)
NOT_DIVIDES_IN_GG(Y, X) → U7_GG(Y, X, div_in_gga(X, Y, U))
NOT_DIVIDES_IN_GG(Y, X) → DIV_IN_GGA(X, Y, U)
DIV_IN_GGA(X, Y, Z) → U1_GGA(X, Y, Z, quot_in_ggga(X, Y, Y, Z))
DIV_IN_GGA(X, Y, Z) → QUOT_IN_GGGA(X, Y, Y, Z)
QUOT_IN_GGGA(s(X), s(Y), Z, U) → U2_GGGA(X, Y, Z, U, quot_in_ggga(X, Y, Z, U))
QUOT_IN_GGGA(s(X), s(Y), Z, U) → QUOT_IN_GGGA(X, Y, Z, U)
QUOT_IN_GGGA(X, 0, s(Z), s(U)) → U3_GGGA(X, Z, U, quot_in_ggga(X, s(Z), s(Z), U))
QUOT_IN_GGGA(X, 0, s(Z), s(U)) → QUOT_IN_GGGA(X, s(Z), s(Z), U)
U7_GG(Y, X, div_out_gga(X, Y, U)) → U8_GG(Y, X, times_in_gga(U, Y, Z))
U7_GG(Y, X, div_out_gga(X, Y, U)) → TIMES_IN_GGA(U, Y, Z)
TIMES_IN_GGA(s(X), Y, Z) → U11_GGA(X, Y, Z, times_in_gga(X, Y, U))
TIMES_IN_GGA(s(X), Y, Z) → TIMES_IN_GGA(X, Y, U)
U11_GGA(X, Y, Z, times_out_gga(X, Y, U)) → U12_GGA(X, Y, Z, add_in_gga(U, Y, Z))
U11_GGA(X, Y, Z, times_out_gga(X, Y, U)) → ADD_IN_GGA(U, Y, Z)
ADD_IN_GGA(s(X), Y, s(Z)) → U13_GGA(X, Y, Z, add_in_gga(X, Y, Z))
ADD_IN_GGA(s(X), Y, s(Z)) → ADD_IN_GGA(X, Y, Z)
U8_GG(Y, X, times_out_gga(U, Y, Z)) → U9_GG(Y, X, neq_in_gg(X, Z))
U8_GG(Y, X, times_out_gga(U, Y, Z)) → NEQ_IN_GG(X, Z)
NEQ_IN_GG(s(X), s(Y)) → U10_GG(X, Y, neq_in_gg(X, Y))
NEQ_IN_GG(s(X), s(Y)) → NEQ_IN_GG(X, Y)
U5_GG(X, Y, not_divides_out_gg(s(s(Y)), X)) → U6_GG(X, Y, pr_in_gg(X, s(Y)))
U5_GG(X, Y, not_divides_out_gg(s(s(Y)), X)) → PR_IN_GG(X, s(Y))

The TRS R consists of the following rules:

prime_in_g(s(s(X))) → U4_g(X, pr_in_gg(s(s(X)), s(X)))
pr_in_gg(X, s(0)) → pr_out_gg(X, s(0))
pr_in_gg(X, s(s(Y))) → U5_gg(X, Y, not_divides_in_gg(s(s(Y)), X))
not_divides_in_gg(Y, X) → U7_gg(Y, X, div_in_gga(X, Y, U))
div_in_gga(X, Y, Z) → U1_gga(X, Y, Z, quot_in_ggga(X, Y, Y, Z))
quot_in_ggga(0, s(Y), s(Z), 0) → quot_out_ggga(0, s(Y), s(Z), 0)
quot_in_ggga(s(X), s(Y), Z, U) → U2_ggga(X, Y, Z, U, quot_in_ggga(X, Y, Z, U))
quot_in_ggga(X, 0, s(Z), s(U)) → U3_ggga(X, Z, U, quot_in_ggga(X, s(Z), s(Z), U))
U3_ggga(X, Z, U, quot_out_ggga(X, s(Z), s(Z), U)) → quot_out_ggga(X, 0, s(Z), s(U))
U2_ggga(X, Y, Z, U, quot_out_ggga(X, Y, Z, U)) → quot_out_ggga(s(X), s(Y), Z, U)
U1_gga(X, Y, Z, quot_out_ggga(X, Y, Y, Z)) → div_out_gga(X, Y, Z)
U7_gg(Y, X, div_out_gga(X, Y, U)) → U8_gg(Y, X, times_in_gga(U, Y, Z))
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U11_gga(X, Y, Z, times_in_gga(X, Y, U))
U11_gga(X, Y, Z, times_out_gga(X, Y, U)) → U12_gga(X, Y, Z, add_in_gga(U, Y, Z))
add_in_gga(X, 0, X) → add_out_gga(X, 0, X)
add_in_gga(0, X, X) → add_out_gga(0, X, X)
add_in_gga(s(X), Y, s(Z)) → U13_gga(X, Y, Z, add_in_gga(X, Y, Z))
U13_gga(X, Y, Z, add_out_gga(X, Y, Z)) → add_out_gga(s(X), Y, s(Z))
U12_gga(X, Y, Z, add_out_gga(U, Y, Z)) → times_out_gga(s(X), Y, Z)
U8_gg(Y, X, times_out_gga(U, Y, Z)) → U9_gg(Y, X, neq_in_gg(X, Z))
neq_in_gg(s(X), 0) → neq_out_gg(s(X), 0)
neq_in_gg(0, s(X)) → neq_out_gg(0, s(X))
neq_in_gg(s(X), s(Y)) → U10_gg(X, Y, neq_in_gg(X, Y))
U10_gg(X, Y, neq_out_gg(X, Y)) → neq_out_gg(s(X), s(Y))
U9_gg(Y, X, neq_out_gg(X, Z)) → not_divides_out_gg(Y, X)
U5_gg(X, Y, not_divides_out_gg(s(s(Y)), X)) → U6_gg(X, Y, pr_in_gg(X, s(Y)))
U6_gg(X, Y, pr_out_gg(X, s(Y))) → pr_out_gg(X, s(s(Y)))
U4_g(X, pr_out_gg(s(s(X)), s(X))) → prime_out_g(s(s(X)))

The argument filtering Pi contains the following mapping:
prime_in_g(x1)  =  prime_in_g(x1)
s(x1)  =  s(x1)
U4_g(x1, x2)  =  U4_g(x2)
pr_in_gg(x1, x2)  =  pr_in_gg(x1, x2)
0  =  0
pr_out_gg(x1, x2)  =  pr_out_gg
U5_gg(x1, x2, x3)  =  U5_gg(x1, x2, x3)
not_divides_in_gg(x1, x2)  =  not_divides_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
div_in_gga(x1, x2, x3)  =  div_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x4)
quot_in_ggga(x1, x2, x3, x4)  =  quot_in_ggga(x1, x2, x3)
quot_out_ggga(x1, x2, x3, x4)  =  quot_out_ggga(x4)
U2_ggga(x1, x2, x3, x4, x5)  =  U2_ggga(x5)
U3_ggga(x1, x2, x3, x4)  =  U3_ggga(x4)
div_out_gga(x1, x2, x3)  =  div_out_gga(x3)
U8_gg(x1, x2, x3)  =  U8_gg(x2, x3)
times_in_gga(x1, x2, x3)  =  times_in_gga(x1, x2)
times_out_gga(x1, x2, x3)  =  times_out_gga(x3)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x2, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
add_in_gga(x1, x2, x3)  =  add_in_gga(x1, x2)
add_out_gga(x1, x2, x3)  =  add_out_gga(x3)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x4)
U9_gg(x1, x2, x3)  =  U9_gg(x3)
neq_in_gg(x1, x2)  =  neq_in_gg(x1, x2)
neq_out_gg(x1, x2)  =  neq_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
not_divides_out_gg(x1, x2)  =  not_divides_out_gg
U6_gg(x1, x2, x3)  =  U6_gg(x3)
prime_out_g(x1)  =  prime_out_g
U5_GG(x1, x2, x3)  =  U5_GG(x1, x2, x3)
DIV_IN_GGA(x1, x2, x3)  =  DIV_IN_GGA(x1, x2)
TIMES_IN_GGA(x1, x2, x3)  =  TIMES_IN_GGA(x1, x2)
QUOT_IN_GGGA(x1, x2, x3, x4)  =  QUOT_IN_GGGA(x1, x2, x3)
U11_GGA(x1, x2, x3, x4)  =  U11_GGA(x2, x4)
NEQ_IN_GG(x1, x2)  =  NEQ_IN_GG(x1, x2)
U2_GGGA(x1, x2, x3, x4, x5)  =  U2_GGGA(x5)
U12_GGA(x1, x2, x3, x4)  =  U12_GGA(x4)
ADD_IN_GGA(x1, x2, x3)  =  ADD_IN_GGA(x1, x2)
U6_GG(x1, x2, x3)  =  U6_GG(x3)
NOT_DIVIDES_IN_GG(x1, x2)  =  NOT_DIVIDES_IN_GG(x1, x2)
U4_G(x1, x2)  =  U4_G(x2)
U9_GG(x1, x2, x3)  =  U9_GG(x3)
PRIME_IN_G(x1)  =  PRIME_IN_G(x1)
U10_GG(x1, x2, x3)  =  U10_GG(x3)
U13_GGA(x1, x2, x3, x4)  =  U13_GGA(x4)
U3_GGGA(x1, x2, x3, x4)  =  U3_GGGA(x4)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x4)
U7_GG(x1, x2, x3)  =  U7_GG(x1, x2, x3)
U8_GG(x1, x2, x3)  =  U8_GG(x2, x3)
PR_IN_GG(x1, x2)  =  PR_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 5 SCCs with 19 less nodes.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

NEQ_IN_GG(s(X), s(Y)) → NEQ_IN_GG(X, Y)

The TRS R consists of the following rules:

prime_in_g(s(s(X))) → U4_g(X, pr_in_gg(s(s(X)), s(X)))
pr_in_gg(X, s(0)) → pr_out_gg(X, s(0))
pr_in_gg(X, s(s(Y))) → U5_gg(X, Y, not_divides_in_gg(s(s(Y)), X))
not_divides_in_gg(Y, X) → U7_gg(Y, X, div_in_gga(X, Y, U))
div_in_gga(X, Y, Z) → U1_gga(X, Y, Z, quot_in_ggga(X, Y, Y, Z))
quot_in_ggga(0, s(Y), s(Z), 0) → quot_out_ggga(0, s(Y), s(Z), 0)
quot_in_ggga(s(X), s(Y), Z, U) → U2_ggga(X, Y, Z, U, quot_in_ggga(X, Y, Z, U))
quot_in_ggga(X, 0, s(Z), s(U)) → U3_ggga(X, Z, U, quot_in_ggga(X, s(Z), s(Z), U))
U3_ggga(X, Z, U, quot_out_ggga(X, s(Z), s(Z), U)) → quot_out_ggga(X, 0, s(Z), s(U))
U2_ggga(X, Y, Z, U, quot_out_ggga(X, Y, Z, U)) → quot_out_ggga(s(X), s(Y), Z, U)
U1_gga(X, Y, Z, quot_out_ggga(X, Y, Y, Z)) → div_out_gga(X, Y, Z)
U7_gg(Y, X, div_out_gga(X, Y, U)) → U8_gg(Y, X, times_in_gga(U, Y, Z))
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U11_gga(X, Y, Z, times_in_gga(X, Y, U))
U11_gga(X, Y, Z, times_out_gga(X, Y, U)) → U12_gga(X, Y, Z, add_in_gga(U, Y, Z))
add_in_gga(X, 0, X) → add_out_gga(X, 0, X)
add_in_gga(0, X, X) → add_out_gga(0, X, X)
add_in_gga(s(X), Y, s(Z)) → U13_gga(X, Y, Z, add_in_gga(X, Y, Z))
U13_gga(X, Y, Z, add_out_gga(X, Y, Z)) → add_out_gga(s(X), Y, s(Z))
U12_gga(X, Y, Z, add_out_gga(U, Y, Z)) → times_out_gga(s(X), Y, Z)
U8_gg(Y, X, times_out_gga(U, Y, Z)) → U9_gg(Y, X, neq_in_gg(X, Z))
neq_in_gg(s(X), 0) → neq_out_gg(s(X), 0)
neq_in_gg(0, s(X)) → neq_out_gg(0, s(X))
neq_in_gg(s(X), s(Y)) → U10_gg(X, Y, neq_in_gg(X, Y))
U10_gg(X, Y, neq_out_gg(X, Y)) → neq_out_gg(s(X), s(Y))
U9_gg(Y, X, neq_out_gg(X, Z)) → not_divides_out_gg(Y, X)
U5_gg(X, Y, not_divides_out_gg(s(s(Y)), X)) → U6_gg(X, Y, pr_in_gg(X, s(Y)))
U6_gg(X, Y, pr_out_gg(X, s(Y))) → pr_out_gg(X, s(s(Y)))
U4_g(X, pr_out_gg(s(s(X)), s(X))) → prime_out_g(s(s(X)))

The argument filtering Pi contains the following mapping:
prime_in_g(x1)  =  prime_in_g(x1)
s(x1)  =  s(x1)
U4_g(x1, x2)  =  U4_g(x2)
pr_in_gg(x1, x2)  =  pr_in_gg(x1, x2)
0  =  0
pr_out_gg(x1, x2)  =  pr_out_gg
U5_gg(x1, x2, x3)  =  U5_gg(x1, x2, x3)
not_divides_in_gg(x1, x2)  =  not_divides_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
div_in_gga(x1, x2, x3)  =  div_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x4)
quot_in_ggga(x1, x2, x3, x4)  =  quot_in_ggga(x1, x2, x3)
quot_out_ggga(x1, x2, x3, x4)  =  quot_out_ggga(x4)
U2_ggga(x1, x2, x3, x4, x5)  =  U2_ggga(x5)
U3_ggga(x1, x2, x3, x4)  =  U3_ggga(x4)
div_out_gga(x1, x2, x3)  =  div_out_gga(x3)
U8_gg(x1, x2, x3)  =  U8_gg(x2, x3)
times_in_gga(x1, x2, x3)  =  times_in_gga(x1, x2)
times_out_gga(x1, x2, x3)  =  times_out_gga(x3)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x2, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
add_in_gga(x1, x2, x3)  =  add_in_gga(x1, x2)
add_out_gga(x1, x2, x3)  =  add_out_gga(x3)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x4)
U9_gg(x1, x2, x3)  =  U9_gg(x3)
neq_in_gg(x1, x2)  =  neq_in_gg(x1, x2)
neq_out_gg(x1, x2)  =  neq_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
not_divides_out_gg(x1, x2)  =  not_divides_out_gg
U6_gg(x1, x2, x3)  =  U6_gg(x3)
prime_out_g(x1)  =  prime_out_g
NEQ_IN_GG(x1, x2)  =  NEQ_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

NEQ_IN_GG(s(X), s(Y)) → NEQ_IN_GG(X, Y)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

NEQ_IN_GG(s(X), s(Y)) → NEQ_IN_GG(X, Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

ADD_IN_GGA(s(X), Y, s(Z)) → ADD_IN_GGA(X, Y, Z)

The TRS R consists of the following rules:

prime_in_g(s(s(X))) → U4_g(X, pr_in_gg(s(s(X)), s(X)))
pr_in_gg(X, s(0)) → pr_out_gg(X, s(0))
pr_in_gg(X, s(s(Y))) → U5_gg(X, Y, not_divides_in_gg(s(s(Y)), X))
not_divides_in_gg(Y, X) → U7_gg(Y, X, div_in_gga(X, Y, U))
div_in_gga(X, Y, Z) → U1_gga(X, Y, Z, quot_in_ggga(X, Y, Y, Z))
quot_in_ggga(0, s(Y), s(Z), 0) → quot_out_ggga(0, s(Y), s(Z), 0)
quot_in_ggga(s(X), s(Y), Z, U) → U2_ggga(X, Y, Z, U, quot_in_ggga(X, Y, Z, U))
quot_in_ggga(X, 0, s(Z), s(U)) → U3_ggga(X, Z, U, quot_in_ggga(X, s(Z), s(Z), U))
U3_ggga(X, Z, U, quot_out_ggga(X, s(Z), s(Z), U)) → quot_out_ggga(X, 0, s(Z), s(U))
U2_ggga(X, Y, Z, U, quot_out_ggga(X, Y, Z, U)) → quot_out_ggga(s(X), s(Y), Z, U)
U1_gga(X, Y, Z, quot_out_ggga(X, Y, Y, Z)) → div_out_gga(X, Y, Z)
U7_gg(Y, X, div_out_gga(X, Y, U)) → U8_gg(Y, X, times_in_gga(U, Y, Z))
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U11_gga(X, Y, Z, times_in_gga(X, Y, U))
U11_gga(X, Y, Z, times_out_gga(X, Y, U)) → U12_gga(X, Y, Z, add_in_gga(U, Y, Z))
add_in_gga(X, 0, X) → add_out_gga(X, 0, X)
add_in_gga(0, X, X) → add_out_gga(0, X, X)
add_in_gga(s(X), Y, s(Z)) → U13_gga(X, Y, Z, add_in_gga(X, Y, Z))
U13_gga(X, Y, Z, add_out_gga(X, Y, Z)) → add_out_gga(s(X), Y, s(Z))
U12_gga(X, Y, Z, add_out_gga(U, Y, Z)) → times_out_gga(s(X), Y, Z)
U8_gg(Y, X, times_out_gga(U, Y, Z)) → U9_gg(Y, X, neq_in_gg(X, Z))
neq_in_gg(s(X), 0) → neq_out_gg(s(X), 0)
neq_in_gg(0, s(X)) → neq_out_gg(0, s(X))
neq_in_gg(s(X), s(Y)) → U10_gg(X, Y, neq_in_gg(X, Y))
U10_gg(X, Y, neq_out_gg(X, Y)) → neq_out_gg(s(X), s(Y))
U9_gg(Y, X, neq_out_gg(X, Z)) → not_divides_out_gg(Y, X)
U5_gg(X, Y, not_divides_out_gg(s(s(Y)), X)) → U6_gg(X, Y, pr_in_gg(X, s(Y)))
U6_gg(X, Y, pr_out_gg(X, s(Y))) → pr_out_gg(X, s(s(Y)))
U4_g(X, pr_out_gg(s(s(X)), s(X))) → prime_out_g(s(s(X)))

The argument filtering Pi contains the following mapping:
prime_in_g(x1)  =  prime_in_g(x1)
s(x1)  =  s(x1)
U4_g(x1, x2)  =  U4_g(x2)
pr_in_gg(x1, x2)  =  pr_in_gg(x1, x2)
0  =  0
pr_out_gg(x1, x2)  =  pr_out_gg
U5_gg(x1, x2, x3)  =  U5_gg(x1, x2, x3)
not_divides_in_gg(x1, x2)  =  not_divides_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
div_in_gga(x1, x2, x3)  =  div_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x4)
quot_in_ggga(x1, x2, x3, x4)  =  quot_in_ggga(x1, x2, x3)
quot_out_ggga(x1, x2, x3, x4)  =  quot_out_ggga(x4)
U2_ggga(x1, x2, x3, x4, x5)  =  U2_ggga(x5)
U3_ggga(x1, x2, x3, x4)  =  U3_ggga(x4)
div_out_gga(x1, x2, x3)  =  div_out_gga(x3)
U8_gg(x1, x2, x3)  =  U8_gg(x2, x3)
times_in_gga(x1, x2, x3)  =  times_in_gga(x1, x2)
times_out_gga(x1, x2, x3)  =  times_out_gga(x3)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x2, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
add_in_gga(x1, x2, x3)  =  add_in_gga(x1, x2)
add_out_gga(x1, x2, x3)  =  add_out_gga(x3)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x4)
U9_gg(x1, x2, x3)  =  U9_gg(x3)
neq_in_gg(x1, x2)  =  neq_in_gg(x1, x2)
neq_out_gg(x1, x2)  =  neq_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
not_divides_out_gg(x1, x2)  =  not_divides_out_gg
U6_gg(x1, x2, x3)  =  U6_gg(x3)
prime_out_g(x1)  =  prime_out_g
ADD_IN_GGA(x1, x2, x3)  =  ADD_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

ADD_IN_GGA(s(X), Y, s(Z)) → ADD_IN_GGA(X, Y, Z)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
ADD_IN_GGA(x1, x2, x3)  =  ADD_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

ADD_IN_GGA(s(X), Y) → ADD_IN_GGA(X, Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

TIMES_IN_GGA(s(X), Y, Z) → TIMES_IN_GGA(X, Y, U)

The TRS R consists of the following rules:

prime_in_g(s(s(X))) → U4_g(X, pr_in_gg(s(s(X)), s(X)))
pr_in_gg(X, s(0)) → pr_out_gg(X, s(0))
pr_in_gg(X, s(s(Y))) → U5_gg(X, Y, not_divides_in_gg(s(s(Y)), X))
not_divides_in_gg(Y, X) → U7_gg(Y, X, div_in_gga(X, Y, U))
div_in_gga(X, Y, Z) → U1_gga(X, Y, Z, quot_in_ggga(X, Y, Y, Z))
quot_in_ggga(0, s(Y), s(Z), 0) → quot_out_ggga(0, s(Y), s(Z), 0)
quot_in_ggga(s(X), s(Y), Z, U) → U2_ggga(X, Y, Z, U, quot_in_ggga(X, Y, Z, U))
quot_in_ggga(X, 0, s(Z), s(U)) → U3_ggga(X, Z, U, quot_in_ggga(X, s(Z), s(Z), U))
U3_ggga(X, Z, U, quot_out_ggga(X, s(Z), s(Z), U)) → quot_out_ggga(X, 0, s(Z), s(U))
U2_ggga(X, Y, Z, U, quot_out_ggga(X, Y, Z, U)) → quot_out_ggga(s(X), s(Y), Z, U)
U1_gga(X, Y, Z, quot_out_ggga(X, Y, Y, Z)) → div_out_gga(X, Y, Z)
U7_gg(Y, X, div_out_gga(X, Y, U)) → U8_gg(Y, X, times_in_gga(U, Y, Z))
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U11_gga(X, Y, Z, times_in_gga(X, Y, U))
U11_gga(X, Y, Z, times_out_gga(X, Y, U)) → U12_gga(X, Y, Z, add_in_gga(U, Y, Z))
add_in_gga(X, 0, X) → add_out_gga(X, 0, X)
add_in_gga(0, X, X) → add_out_gga(0, X, X)
add_in_gga(s(X), Y, s(Z)) → U13_gga(X, Y, Z, add_in_gga(X, Y, Z))
U13_gga(X, Y, Z, add_out_gga(X, Y, Z)) → add_out_gga(s(X), Y, s(Z))
U12_gga(X, Y, Z, add_out_gga(U, Y, Z)) → times_out_gga(s(X), Y, Z)
U8_gg(Y, X, times_out_gga(U, Y, Z)) → U9_gg(Y, X, neq_in_gg(X, Z))
neq_in_gg(s(X), 0) → neq_out_gg(s(X), 0)
neq_in_gg(0, s(X)) → neq_out_gg(0, s(X))
neq_in_gg(s(X), s(Y)) → U10_gg(X, Y, neq_in_gg(X, Y))
U10_gg(X, Y, neq_out_gg(X, Y)) → neq_out_gg(s(X), s(Y))
U9_gg(Y, X, neq_out_gg(X, Z)) → not_divides_out_gg(Y, X)
U5_gg(X, Y, not_divides_out_gg(s(s(Y)), X)) → U6_gg(X, Y, pr_in_gg(X, s(Y)))
U6_gg(X, Y, pr_out_gg(X, s(Y))) → pr_out_gg(X, s(s(Y)))
U4_g(X, pr_out_gg(s(s(X)), s(X))) → prime_out_g(s(s(X)))

The argument filtering Pi contains the following mapping:
prime_in_g(x1)  =  prime_in_g(x1)
s(x1)  =  s(x1)
U4_g(x1, x2)  =  U4_g(x2)
pr_in_gg(x1, x2)  =  pr_in_gg(x1, x2)
0  =  0
pr_out_gg(x1, x2)  =  pr_out_gg
U5_gg(x1, x2, x3)  =  U5_gg(x1, x2, x3)
not_divides_in_gg(x1, x2)  =  not_divides_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
div_in_gga(x1, x2, x3)  =  div_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x4)
quot_in_ggga(x1, x2, x3, x4)  =  quot_in_ggga(x1, x2, x3)
quot_out_ggga(x1, x2, x3, x4)  =  quot_out_ggga(x4)
U2_ggga(x1, x2, x3, x4, x5)  =  U2_ggga(x5)
U3_ggga(x1, x2, x3, x4)  =  U3_ggga(x4)
div_out_gga(x1, x2, x3)  =  div_out_gga(x3)
U8_gg(x1, x2, x3)  =  U8_gg(x2, x3)
times_in_gga(x1, x2, x3)  =  times_in_gga(x1, x2)
times_out_gga(x1, x2, x3)  =  times_out_gga(x3)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x2, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
add_in_gga(x1, x2, x3)  =  add_in_gga(x1, x2)
add_out_gga(x1, x2, x3)  =  add_out_gga(x3)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x4)
U9_gg(x1, x2, x3)  =  U9_gg(x3)
neq_in_gg(x1, x2)  =  neq_in_gg(x1, x2)
neq_out_gg(x1, x2)  =  neq_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
not_divides_out_gg(x1, x2)  =  not_divides_out_gg
U6_gg(x1, x2, x3)  =  U6_gg(x3)
prime_out_g(x1)  =  prime_out_g
TIMES_IN_GGA(x1, x2, x3)  =  TIMES_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

TIMES_IN_GGA(s(X), Y, Z) → TIMES_IN_GGA(X, Y, U)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
TIMES_IN_GGA(x1, x2, x3)  =  TIMES_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

TIMES_IN_GGA(s(X), Y) → TIMES_IN_GGA(X, Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

QUOT_IN_GGGA(X, 0, s(Z), s(U)) → QUOT_IN_GGGA(X, s(Z), s(Z), U)
QUOT_IN_GGGA(s(X), s(Y), Z, U) → QUOT_IN_GGGA(X, Y, Z, U)

The TRS R consists of the following rules:

prime_in_g(s(s(X))) → U4_g(X, pr_in_gg(s(s(X)), s(X)))
pr_in_gg(X, s(0)) → pr_out_gg(X, s(0))
pr_in_gg(X, s(s(Y))) → U5_gg(X, Y, not_divides_in_gg(s(s(Y)), X))
not_divides_in_gg(Y, X) → U7_gg(Y, X, div_in_gga(X, Y, U))
div_in_gga(X, Y, Z) → U1_gga(X, Y, Z, quot_in_ggga(X, Y, Y, Z))
quot_in_ggga(0, s(Y), s(Z), 0) → quot_out_ggga(0, s(Y), s(Z), 0)
quot_in_ggga(s(X), s(Y), Z, U) → U2_ggga(X, Y, Z, U, quot_in_ggga(X, Y, Z, U))
quot_in_ggga(X, 0, s(Z), s(U)) → U3_ggga(X, Z, U, quot_in_ggga(X, s(Z), s(Z), U))
U3_ggga(X, Z, U, quot_out_ggga(X, s(Z), s(Z), U)) → quot_out_ggga(X, 0, s(Z), s(U))
U2_ggga(X, Y, Z, U, quot_out_ggga(X, Y, Z, U)) → quot_out_ggga(s(X), s(Y), Z, U)
U1_gga(X, Y, Z, quot_out_ggga(X, Y, Y, Z)) → div_out_gga(X, Y, Z)
U7_gg(Y, X, div_out_gga(X, Y, U)) → U8_gg(Y, X, times_in_gga(U, Y, Z))
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U11_gga(X, Y, Z, times_in_gga(X, Y, U))
U11_gga(X, Y, Z, times_out_gga(X, Y, U)) → U12_gga(X, Y, Z, add_in_gga(U, Y, Z))
add_in_gga(X, 0, X) → add_out_gga(X, 0, X)
add_in_gga(0, X, X) → add_out_gga(0, X, X)
add_in_gga(s(X), Y, s(Z)) → U13_gga(X, Y, Z, add_in_gga(X, Y, Z))
U13_gga(X, Y, Z, add_out_gga(X, Y, Z)) → add_out_gga(s(X), Y, s(Z))
U12_gga(X, Y, Z, add_out_gga(U, Y, Z)) → times_out_gga(s(X), Y, Z)
U8_gg(Y, X, times_out_gga(U, Y, Z)) → U9_gg(Y, X, neq_in_gg(X, Z))
neq_in_gg(s(X), 0) → neq_out_gg(s(X), 0)
neq_in_gg(0, s(X)) → neq_out_gg(0, s(X))
neq_in_gg(s(X), s(Y)) → U10_gg(X, Y, neq_in_gg(X, Y))
U10_gg(X, Y, neq_out_gg(X, Y)) → neq_out_gg(s(X), s(Y))
U9_gg(Y, X, neq_out_gg(X, Z)) → not_divides_out_gg(Y, X)
U5_gg(X, Y, not_divides_out_gg(s(s(Y)), X)) → U6_gg(X, Y, pr_in_gg(X, s(Y)))
U6_gg(X, Y, pr_out_gg(X, s(Y))) → pr_out_gg(X, s(s(Y)))
U4_g(X, pr_out_gg(s(s(X)), s(X))) → prime_out_g(s(s(X)))

The argument filtering Pi contains the following mapping:
prime_in_g(x1)  =  prime_in_g(x1)
s(x1)  =  s(x1)
U4_g(x1, x2)  =  U4_g(x2)
pr_in_gg(x1, x2)  =  pr_in_gg(x1, x2)
0  =  0
pr_out_gg(x1, x2)  =  pr_out_gg
U5_gg(x1, x2, x3)  =  U5_gg(x1, x2, x3)
not_divides_in_gg(x1, x2)  =  not_divides_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
div_in_gga(x1, x2, x3)  =  div_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x4)
quot_in_ggga(x1, x2, x3, x4)  =  quot_in_ggga(x1, x2, x3)
quot_out_ggga(x1, x2, x3, x4)  =  quot_out_ggga(x4)
U2_ggga(x1, x2, x3, x4, x5)  =  U2_ggga(x5)
U3_ggga(x1, x2, x3, x4)  =  U3_ggga(x4)
div_out_gga(x1, x2, x3)  =  div_out_gga(x3)
U8_gg(x1, x2, x3)  =  U8_gg(x2, x3)
times_in_gga(x1, x2, x3)  =  times_in_gga(x1, x2)
times_out_gga(x1, x2, x3)  =  times_out_gga(x3)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x2, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
add_in_gga(x1, x2, x3)  =  add_in_gga(x1, x2)
add_out_gga(x1, x2, x3)  =  add_out_gga(x3)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x4)
U9_gg(x1, x2, x3)  =  U9_gg(x3)
neq_in_gg(x1, x2)  =  neq_in_gg(x1, x2)
neq_out_gg(x1, x2)  =  neq_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
not_divides_out_gg(x1, x2)  =  not_divides_out_gg
U6_gg(x1, x2, x3)  =  U6_gg(x3)
prime_out_g(x1)  =  prime_out_g
QUOT_IN_GGGA(x1, x2, x3, x4)  =  QUOT_IN_GGGA(x1, x2, x3)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

QUOT_IN_GGGA(X, 0, s(Z), s(U)) → QUOT_IN_GGGA(X, s(Z), s(Z), U)
QUOT_IN_GGGA(s(X), s(Y), Z, U) → QUOT_IN_GGGA(X, Y, Z, U)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
QUOT_IN_GGGA(x1, x2, x3, x4)  =  QUOT_IN_GGGA(x1, x2, x3)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

QUOT_IN_GGGA(X, 0, s(Z)) → QUOT_IN_GGGA(X, s(Z), s(Z))
QUOT_IN_GGGA(s(X), s(Y), Z) → QUOT_IN_GGGA(X, Y, Z)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof

Pi DP problem:
The TRS P consists of the following rules:

U5_GG(X, Y, not_divides_out_gg(s(s(Y)), X)) → PR_IN_GG(X, s(Y))
PR_IN_GG(X, s(s(Y))) → U5_GG(X, Y, not_divides_in_gg(s(s(Y)), X))

The TRS R consists of the following rules:

prime_in_g(s(s(X))) → U4_g(X, pr_in_gg(s(s(X)), s(X)))
pr_in_gg(X, s(0)) → pr_out_gg(X, s(0))
pr_in_gg(X, s(s(Y))) → U5_gg(X, Y, not_divides_in_gg(s(s(Y)), X))
not_divides_in_gg(Y, X) → U7_gg(Y, X, div_in_gga(X, Y, U))
div_in_gga(X, Y, Z) → U1_gga(X, Y, Z, quot_in_ggga(X, Y, Y, Z))
quot_in_ggga(0, s(Y), s(Z), 0) → quot_out_ggga(0, s(Y), s(Z), 0)
quot_in_ggga(s(X), s(Y), Z, U) → U2_ggga(X, Y, Z, U, quot_in_ggga(X, Y, Z, U))
quot_in_ggga(X, 0, s(Z), s(U)) → U3_ggga(X, Z, U, quot_in_ggga(X, s(Z), s(Z), U))
U3_ggga(X, Z, U, quot_out_ggga(X, s(Z), s(Z), U)) → quot_out_ggga(X, 0, s(Z), s(U))
U2_ggga(X, Y, Z, U, quot_out_ggga(X, Y, Z, U)) → quot_out_ggga(s(X), s(Y), Z, U)
U1_gga(X, Y, Z, quot_out_ggga(X, Y, Y, Z)) → div_out_gga(X, Y, Z)
U7_gg(Y, X, div_out_gga(X, Y, U)) → U8_gg(Y, X, times_in_gga(U, Y, Z))
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U11_gga(X, Y, Z, times_in_gga(X, Y, U))
U11_gga(X, Y, Z, times_out_gga(X, Y, U)) → U12_gga(X, Y, Z, add_in_gga(U, Y, Z))
add_in_gga(X, 0, X) → add_out_gga(X, 0, X)
add_in_gga(0, X, X) → add_out_gga(0, X, X)
add_in_gga(s(X), Y, s(Z)) → U13_gga(X, Y, Z, add_in_gga(X, Y, Z))
U13_gga(X, Y, Z, add_out_gga(X, Y, Z)) → add_out_gga(s(X), Y, s(Z))
U12_gga(X, Y, Z, add_out_gga(U, Y, Z)) → times_out_gga(s(X), Y, Z)
U8_gg(Y, X, times_out_gga(U, Y, Z)) → U9_gg(Y, X, neq_in_gg(X, Z))
neq_in_gg(s(X), 0) → neq_out_gg(s(X), 0)
neq_in_gg(0, s(X)) → neq_out_gg(0, s(X))
neq_in_gg(s(X), s(Y)) → U10_gg(X, Y, neq_in_gg(X, Y))
U10_gg(X, Y, neq_out_gg(X, Y)) → neq_out_gg(s(X), s(Y))
U9_gg(Y, X, neq_out_gg(X, Z)) → not_divides_out_gg(Y, X)
U5_gg(X, Y, not_divides_out_gg(s(s(Y)), X)) → U6_gg(X, Y, pr_in_gg(X, s(Y)))
U6_gg(X, Y, pr_out_gg(X, s(Y))) → pr_out_gg(X, s(s(Y)))
U4_g(X, pr_out_gg(s(s(X)), s(X))) → prime_out_g(s(s(X)))

The argument filtering Pi contains the following mapping:
prime_in_g(x1)  =  prime_in_g(x1)
s(x1)  =  s(x1)
U4_g(x1, x2)  =  U4_g(x2)
pr_in_gg(x1, x2)  =  pr_in_gg(x1, x2)
0  =  0
pr_out_gg(x1, x2)  =  pr_out_gg
U5_gg(x1, x2, x3)  =  U5_gg(x1, x2, x3)
not_divides_in_gg(x1, x2)  =  not_divides_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
div_in_gga(x1, x2, x3)  =  div_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x4)
quot_in_ggga(x1, x2, x3, x4)  =  quot_in_ggga(x1, x2, x3)
quot_out_ggga(x1, x2, x3, x4)  =  quot_out_ggga(x4)
U2_ggga(x1, x2, x3, x4, x5)  =  U2_ggga(x5)
U3_ggga(x1, x2, x3, x4)  =  U3_ggga(x4)
div_out_gga(x1, x2, x3)  =  div_out_gga(x3)
U8_gg(x1, x2, x3)  =  U8_gg(x2, x3)
times_in_gga(x1, x2, x3)  =  times_in_gga(x1, x2)
times_out_gga(x1, x2, x3)  =  times_out_gga(x3)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x2, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
add_in_gga(x1, x2, x3)  =  add_in_gga(x1, x2)
add_out_gga(x1, x2, x3)  =  add_out_gga(x3)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x4)
U9_gg(x1, x2, x3)  =  U9_gg(x3)
neq_in_gg(x1, x2)  =  neq_in_gg(x1, x2)
neq_out_gg(x1, x2)  =  neq_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
not_divides_out_gg(x1, x2)  =  not_divides_out_gg
U6_gg(x1, x2, x3)  =  U6_gg(x3)
prime_out_g(x1)  =  prime_out_g
U5_GG(x1, x2, x3)  =  U5_GG(x1, x2, x3)
PR_IN_GG(x1, x2)  =  PR_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

U5_GG(X, Y, not_divides_out_gg(s(s(Y)), X)) → PR_IN_GG(X, s(Y))
PR_IN_GG(X, s(s(Y))) → U5_GG(X, Y, not_divides_in_gg(s(s(Y)), X))

The TRS R consists of the following rules:

not_divides_in_gg(Y, X) → U7_gg(Y, X, div_in_gga(X, Y, U))
U7_gg(Y, X, div_out_gga(X, Y, U)) → U8_gg(Y, X, times_in_gga(U, Y, Z))
div_in_gga(X, Y, Z) → U1_gga(X, Y, Z, quot_in_ggga(X, Y, Y, Z))
U8_gg(Y, X, times_out_gga(U, Y, Z)) → U9_gg(Y, X, neq_in_gg(X, Z))
U1_gga(X, Y, Z, quot_out_ggga(X, Y, Y, Z)) → div_out_gga(X, Y, Z)
times_in_gga(0, Y, 0) → times_out_gga(0, Y, 0)
times_in_gga(s(X), Y, Z) → U11_gga(X, Y, Z, times_in_gga(X, Y, U))
U9_gg(Y, X, neq_out_gg(X, Z)) → not_divides_out_gg(Y, X)
quot_in_ggga(0, s(Y), s(Z), 0) → quot_out_ggga(0, s(Y), s(Z), 0)
quot_in_ggga(s(X), s(Y), Z, U) → U2_ggga(X, Y, Z, U, quot_in_ggga(X, Y, Z, U))
quot_in_ggga(X, 0, s(Z), s(U)) → U3_ggga(X, Z, U, quot_in_ggga(X, s(Z), s(Z), U))
U11_gga(X, Y, Z, times_out_gga(X, Y, U)) → U12_gga(X, Y, Z, add_in_gga(U, Y, Z))
neq_in_gg(s(X), 0) → neq_out_gg(s(X), 0)
neq_in_gg(0, s(X)) → neq_out_gg(0, s(X))
neq_in_gg(s(X), s(Y)) → U10_gg(X, Y, neq_in_gg(X, Y))
U2_ggga(X, Y, Z, U, quot_out_ggga(X, Y, Z, U)) → quot_out_ggga(s(X), s(Y), Z, U)
U3_ggga(X, Z, U, quot_out_ggga(X, s(Z), s(Z), U)) → quot_out_ggga(X, 0, s(Z), s(U))
U12_gga(X, Y, Z, add_out_gga(U, Y, Z)) → times_out_gga(s(X), Y, Z)
U10_gg(X, Y, neq_out_gg(X, Y)) → neq_out_gg(s(X), s(Y))
add_in_gga(X, 0, X) → add_out_gga(X, 0, X)
add_in_gga(0, X, X) → add_out_gga(0, X, X)
add_in_gga(s(X), Y, s(Z)) → U13_gga(X, Y, Z, add_in_gga(X, Y, Z))
U13_gga(X, Y, Z, add_out_gga(X, Y, Z)) → add_out_gga(s(X), Y, s(Z))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
not_divides_in_gg(x1, x2)  =  not_divides_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
div_in_gga(x1, x2, x3)  =  div_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x4)
quot_in_ggga(x1, x2, x3, x4)  =  quot_in_ggga(x1, x2, x3)
quot_out_ggga(x1, x2, x3, x4)  =  quot_out_ggga(x4)
U2_ggga(x1, x2, x3, x4, x5)  =  U2_ggga(x5)
U3_ggga(x1, x2, x3, x4)  =  U3_ggga(x4)
div_out_gga(x1, x2, x3)  =  div_out_gga(x3)
U8_gg(x1, x2, x3)  =  U8_gg(x2, x3)
times_in_gga(x1, x2, x3)  =  times_in_gga(x1, x2)
times_out_gga(x1, x2, x3)  =  times_out_gga(x3)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x2, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
add_in_gga(x1, x2, x3)  =  add_in_gga(x1, x2)
add_out_gga(x1, x2, x3)  =  add_out_gga(x3)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x4)
U9_gg(x1, x2, x3)  =  U9_gg(x3)
neq_in_gg(x1, x2)  =  neq_in_gg(x1, x2)
neq_out_gg(x1, x2)  =  neq_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
not_divides_out_gg(x1, x2)  =  not_divides_out_gg
U5_GG(x1, x2, x3)  =  U5_GG(x1, x2, x3)
PR_IN_GG(x1, x2)  =  PR_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

PR_IN_GG(X, s(s(Y))) → U5_GG(X, Y, not_divides_in_gg(s(s(Y)), X))
U5_GG(X, Y, not_divides_out_gg) → PR_IN_GG(X, s(Y))

The TRS R consists of the following rules:

not_divides_in_gg(Y, X) → U7_gg(Y, X, div_in_gga(X, Y))
U7_gg(Y, X, div_out_gga(U)) → U8_gg(X, times_in_gga(U, Y))
div_in_gga(X, Y) → U1_gga(quot_in_ggga(X, Y, Y))
U8_gg(X, times_out_gga(Z)) → U9_gg(neq_in_gg(X, Z))
U1_gga(quot_out_ggga(Z)) → div_out_gga(Z)
times_in_gga(0, Y) → times_out_gga(0)
times_in_gga(s(X), Y) → U11_gga(Y, times_in_gga(X, Y))
U9_gg(neq_out_gg) → not_divides_out_gg
quot_in_ggga(0, s(Y), s(Z)) → quot_out_ggga(0)
quot_in_ggga(s(X), s(Y), Z) → U2_ggga(quot_in_ggga(X, Y, Z))
quot_in_ggga(X, 0, s(Z)) → U3_ggga(quot_in_ggga(X, s(Z), s(Z)))
U11_gga(Y, times_out_gga(U)) → U12_gga(add_in_gga(U, Y))
neq_in_gg(s(X), 0) → neq_out_gg
neq_in_gg(0, s(X)) → neq_out_gg
neq_in_gg(s(X), s(Y)) → U10_gg(neq_in_gg(X, Y))
U2_ggga(quot_out_ggga(U)) → quot_out_ggga(U)
U3_ggga(quot_out_ggga(U)) → quot_out_ggga(s(U))
U12_gga(add_out_gga(Z)) → times_out_gga(Z)
U10_gg(neq_out_gg) → neq_out_gg
add_in_gga(X, 0) → add_out_gga(X)
add_in_gga(0, X) → add_out_gga(X)
add_in_gga(s(X), Y) → U13_gga(add_in_gga(X, Y))
U13_gga(add_out_gga(Z)) → add_out_gga(s(Z))

The set Q consists of the following terms:

not_divides_in_gg(x0, x1)
U7_gg(x0, x1, x2)
div_in_gga(x0, x1)
U8_gg(x0, x1)
U1_gga(x0)
times_in_gga(x0, x1)
U9_gg(x0)
quot_in_ggga(x0, x1, x2)
U11_gga(x0, x1)
neq_in_gg(x0, x1)
U2_ggga(x0)
U3_ggga(x0)
U12_gga(x0)
U10_gg(x0)
add_in_gga(x0, x1)
U13_gga(x0)

We have to consider all (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


U5_GG(X, Y, not_divides_out_gg) → PR_IN_GG(X, s(Y))
The remaining pairs can at least be oriented weakly.

PR_IN_GG(X, s(s(Y))) → U5_GG(X, Y, not_divides_in_gg(s(s(Y)), X))
Used ordering: Polynomial interpretation [25]:

POL(0) = 1   
POL(PR_IN_GG(x1, x2)) = x2   
POL(U10_gg(x1)) = 0   
POL(U11_gga(x1, x2)) = 0   
POL(U12_gga(x1)) = 0   
POL(U13_gga(x1)) = 1   
POL(U1_gga(x1)) = 0   
POL(U2_ggga(x1)) = 0   
POL(U3_ggga(x1)) = 0   
POL(U5_GG(x1, x2, x3)) = 1 + x2 + x3   
POL(U7_gg(x1, x2, x3)) = 1   
POL(U8_gg(x1, x2)) = 1   
POL(U9_gg(x1)) = 1   
POL(add_in_gga(x1, x2)) = 1 + x2   
POL(add_out_gga(x1)) = 1   
POL(div_in_gga(x1, x2)) = 0   
POL(div_out_gga(x1)) = 0   
POL(neq_in_gg(x1, x2)) = 0   
POL(neq_out_gg) = 0   
POL(not_divides_in_gg(x1, x2)) = 1   
POL(not_divides_out_gg) = 1   
POL(quot_in_ggga(x1, x2, x3)) = 0   
POL(quot_out_ggga(x1)) = 0   
POL(s(x1)) = 1 + x1   
POL(times_in_gga(x1, x2)) = 0   
POL(times_out_gga(x1)) = 0   

The following usable rules [17] were oriented:

U8_gg(X, times_out_gga(Z)) → U9_gg(neq_in_gg(X, Z))
U7_gg(Y, X, div_out_gga(U)) → U8_gg(X, times_in_gga(U, Y))
not_divides_in_gg(Y, X) → U7_gg(Y, X, div_in_gga(X, Y))
U9_gg(neq_out_gg) → not_divides_out_gg



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPOrderProof
                          ↳ QDP
                            ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

PR_IN_GG(X, s(s(Y))) → U5_GG(X, Y, not_divides_in_gg(s(s(Y)), X))

The TRS R consists of the following rules:

not_divides_in_gg(Y, X) → U7_gg(Y, X, div_in_gga(X, Y))
U7_gg(Y, X, div_out_gga(U)) → U8_gg(X, times_in_gga(U, Y))
div_in_gga(X, Y) → U1_gga(quot_in_ggga(X, Y, Y))
U8_gg(X, times_out_gga(Z)) → U9_gg(neq_in_gg(X, Z))
U1_gga(quot_out_ggga(Z)) → div_out_gga(Z)
times_in_gga(0, Y) → times_out_gga(0)
times_in_gga(s(X), Y) → U11_gga(Y, times_in_gga(X, Y))
U9_gg(neq_out_gg) → not_divides_out_gg
quot_in_ggga(0, s(Y), s(Z)) → quot_out_ggga(0)
quot_in_ggga(s(X), s(Y), Z) → U2_ggga(quot_in_ggga(X, Y, Z))
quot_in_ggga(X, 0, s(Z)) → U3_ggga(quot_in_ggga(X, s(Z), s(Z)))
U11_gga(Y, times_out_gga(U)) → U12_gga(add_in_gga(U, Y))
neq_in_gg(s(X), 0) → neq_out_gg
neq_in_gg(0, s(X)) → neq_out_gg
neq_in_gg(s(X), s(Y)) → U10_gg(neq_in_gg(X, Y))
U2_ggga(quot_out_ggga(U)) → quot_out_ggga(U)
U3_ggga(quot_out_ggga(U)) → quot_out_ggga(s(U))
U12_gga(add_out_gga(Z)) → times_out_gga(Z)
U10_gg(neq_out_gg) → neq_out_gg
add_in_gga(X, 0) → add_out_gga(X)
add_in_gga(0, X) → add_out_gga(X)
add_in_gga(s(X), Y) → U13_gga(add_in_gga(X, Y))
U13_gga(add_out_gga(Z)) → add_out_gga(s(Z))

The set Q consists of the following terms:

not_divides_in_gg(x0, x1)
U7_gg(x0, x1, x2)
div_in_gga(x0, x1)
U8_gg(x0, x1)
U1_gga(x0)
times_in_gga(x0, x1)
U9_gg(x0)
quot_in_ggga(x0, x1, x2)
U11_gga(x0, x1)
neq_in_gg(x0, x1)
U2_ggga(x0)
U3_ggga(x0)
U12_gga(x0)
U10_gg(x0)
add_in_gga(x0, x1)
U13_gga(x0)

We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 1 less node.